| 1: | a__minus(0,Y) | → 0 | |
| 2: | a__minus(s(X),s(Y)) | → a__minus(X,Y) | |
| 3: | a__geq(X,0) | → true | |
| 4: | a__geq(0,s(Y)) | → false | |
| 5: | a__geq(s(X),s(Y)) | → a__geq(X,Y) | |
| 6: | a__div(0,s(Y)) | → 0 | |
| 7: | a__div(s(X),s(Y)) | → a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0) | |
| 8: | a__if(true,X,Y) | → mark(X) | |
| 9: | a__if(false,X,Y) | → mark(Y) | |
| 10: | mark(minus(X1,X2)) | → a__minus(X1,X2) | |
| 11: | mark(geq(X1,X2)) | → a__geq(X1,X2) | |
| 12: | mark(div(X1,X2)) | → a__div(mark(X1),X2) | |
| 13: | mark(if(X1,X2,X3)) | → a__if(mark(X1),X2,X3) | |
| 14: | mark(0) | → 0 | |
| 15: | mark(s(X)) | → s(mark(X)) | |
| 16: | mark(true) | → true | |
| 17: | mark(false) | → false | |
| 18: | a__minus(X1,X2) | → minus(X1,X2) | |
| 19: | a__geq(X1,X2) | → geq(X1,X2) | |
| 20: | a__div(X1,X2) | → div(X1,X2) | |
| 21: | a__if(X1,X2,X3) | → if(X1,X2,X3) | |
| 22: | A__MINUS(s(X),s(Y)) | → A__MINUS(X,Y) | |
| 23: | A__GEQ(s(X),s(Y)) | → A__GEQ(X,Y) | |
| 24: | A__DIV(s(X),s(Y)) | → A__IF(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0) | |
| 25: | A__DIV(s(X),s(Y)) | → A__GEQ(X,Y) | |
| 26: | A__IF(true,X,Y) | → MARK(X) | |
| 27: | A__IF(false,X,Y) | → MARK(Y) | |
| 28: | MARK(minus(X1,X2)) | → A__MINUS(X1,X2) | |
| 29: | MARK(geq(X1,X2)) | → A__GEQ(X1,X2) | |
| 30: | MARK(div(X1,X2)) | → A__DIV(mark(X1),X2) | |
| 31: | MARK(div(X1,X2)) | → MARK(X1) | |
| 32: | MARK(if(X1,X2,X3)) | → A__IF(mark(X1),X2,X3) | |
| 33: | MARK(if(X1,X2,X3)) | → MARK(X1) | |
| 34: | MARK(s(X)) | → MARK(X) | |